1. Technical Field
The present invention relates to software analysis and, more particularly, to verifying a safety reachability property in already-deployed systems.
2. Description of the Related Art
Analyzing the runtime behavior of large scale computer systems is challenging due to the lack of availability of accurate models describing the structure and behavior of such systems. Even when models exist, they usually pertain to an old configuration of the system and do not include all changes made after the system was deployed and tuned. Moreover, it is often hard to get access to the actual system to carry out such modeling/analysis. Typically all one has access to is system logs and traces.
Hidden Markov models have been extracted from a given set of logs using a variety of extant techniques. However, existing techniques mainly infer one Markov model which assigns concrete probabilities to transitions of the model. Realistically speaking, however, it is very difficult to deduce a precise Markov model from only a finite set of systems logs, as the deduced probabilities will have uncertainties which existing techniques fail to take into account.